$\forall$$T$:Type. $T$ $\subseteq\rho$ $\mathbb{Z}$ $\Rightarrow$ ($\forall$$L$:$T$ List. sorted($L$) $\in$ Prop)